Inductive ArithEval (s: State) : ArithExp -> Integer -> Prop :=
  | arith_eval_num   : forall (n:Integer),
      ArithEval s (arith_exp_num n) n

  | arith_eval_id    : forall (i:Id)(z:Integer),
      s i = Some (int_val z) -> ArithEval s (arith_exp_id i)  z

  | arith_eval_plus  : forall (e1 e2: ArithExp) (n1 n2 : Integer), 
      ArithEval s e1 n1 -> ArithEval s e2 n2 -> ArithEval s (arith_exp_plus e1 e2) (int_plus n1 n2) 

  | arith_eval_minus : forall (e1 e2: ArithExp) (n1 n2 : Integer), 
      ArithEval s e1 n1 -> ArithEval s e2 n2 -> ArithEval s (arith_exp_minus e1 e2) (int_minus n1 n2) 

  | arith_eval_mult  : forall (e1 e2: ArithExp) (n1 n2 : Integer), 
      ArithEval s e1 n1 -> ArithEval s e2 n2 -> ArithEval s (arith_exp_mult e1 e2) (int_mult n1 n2)

  | arith_eval_div   : forall (e1 e2: ArithExp) (n1 n2 : Integer),
      ArithEval s e1 n1 -> ArithEval s e2 n2 -> ArithEval s (arith_exp_div e1 e2) (int_div n1 n2)

  | arith_eval_mod   : forall (e1 e2: ArithExp) (n1 n2 : Integer),
      ArithEval s e1 n1 -> ArithEval s e2 n2 -> ArithEval s (arith_exp_mod e1 e2) (int_modulo n1 n2)
.